[WIP] Calldata generation for bytes, bytes[] parameters
#2265
+329
−22
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* lemmas on Boolean reasoning, set reasoning, map lookup, and keccak * Set Version: 1.0.277 * removing keccak lemmas that should not be upstreamed * addressing comments * Set Version: 1.0.278 * Set Version: 1.0.278 * corrections * removing ==Bool from expected files * Set Version: 1.0.279 * Set Version: 1.0.279 * Set Version: 1.0.309 * Set Version: 1.0.311 * updating expected outputs * Set Version: 1.0.312 * Set Version: 1.0.330 * Set Version: 1.0.334 * revisiting set simplifications * --amend * --amend * --amend * streamlining lookup simplifications * streamlining set simplifications * removing set reasoning entirely * Set Version: 1.0.336 * concretising set simplifications: * streamlining set simplifications * Set Version: 1.0.337 * even more concrete set simplifications * bringing old simplifications back * Set Version: 1.0.340 * resolving parsing ambiguities * --amend * --amend * Set Version: 1.0.341 * Set Version: 1.0.342 * Set Version: 1.0.343 * correction * syntax * --amend * Set Version: 1.0.349 * Set Version: 1.0.355 * Set Version: 1.0.356 * Set Version: 1.0.357 * Correctly ordered arguments in `typed_args` (#2174) * Correctly ordered arguments in `typed_args` * Set Version: 1.0.357 --------- Co-authored-by: devops <[email protected]> * Inject `ccopts` directly into `kevm_kompile` and fix some tests (#2164) * Makefile: make sure evm-optimizations-spec is rebuilt on changes to optimizations.md * kproj/optimizations: remove symbolic attribute on evm-optimizations-lemmas * tests/specs/examples/sum-to-n-foundry-spec: correct imports for LLVM backend * tests/specs/functional/infinite-gas-spec.k: allow import of main module in symbolic module for LLVM * kevm-pyk/__main__, Makefile, VERIFICATION: rename kevm {kompile => kompile-spec} for more accurate usage * README: update documentation * kevm-pyk/: all builds require plugin_dir, compute it directly * kevm-pyk/: move calculation of plugin_dir out of run_kompile, pass in ccopts directly * kevm-pyk/__main__: adjust acceptable values for kevm kompile-spec * VERIFICATION: update documentation * Makefile: bring back --target argument * Set Version: 1.0.343 * test_prove: only add ccopts if were using the booster * Set Version: 1.0.355 * package/test-package: add previously failing test of using booster due to plugin_dir being missing * kevm-pyk/__main__: use correct target for kompile-spec * Set Version: 1.0.356 * Set Version: 1.0.356 * kevm-pyk/plugin: correction from code review * kevm-pyk/kdist/plugin: hardcode plugin as dependency for other targets * kevm-pyk/: factor out generic run_kompile from kevm_kompile * kevm_pyk/kompile: rename lib_ccopts => _lib_ccopts * Set Version: 1.0.357 * kevm-pyk/kdist/plugin: make sure all KEVMTarget have plugin as depenndency * Set Version: 1.0.357 * kdist/plugin: drop self._deps * Set Version: 1.0.358 * Set Version: 1.0.358 --------- Co-authored-by: devops <[email protected]> * Fix circular import (#2179) * Fix circular import * Set Version: 1.0.359 --------- Co-authored-by: devops <[email protected]> * Move `--port` arguments to `rpc_args` (#2178) * Move `--port` arguments to `rpc_args` * Set Version: 1.0.359 * Set Version: 1.0.360 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> * Update dependency: deps/pyk_release (#2175) * deps/pyk_release: Set Version v0.1.501 * Set Version: 1.0.357 * kevm-pyk/: sync poetry files pyk version v0.1.501 * deps/k_release: sync release file version 6.1.14 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.359 * kevm-pyk/: sync poetry files pyk version v0.1.501 * Set Version: 1.0.361 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> * Update dependency: deps/pyk_release (#2181) * deps/pyk_release: Set Version v0.1.505 * kevm-pyk/: sync poetry files pyk version v0.1.505 * deps/k_release: sync release file version 6.1.20 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.362 --------- Co-authored-by: devops <[email protected]> * Set Version: 1.0.364 * Set Version: 1.0.364 * Set Version: 1.0.365 * Set Version: 1.0.372 * Set Version: 1.0.379 * adding tests * Set Version: 1.0.381 * normalising comparisons, adding keccak * reverting normalisation * removing equality simplification * Set Version: 1.0.382 * Set Version: 1.0.382 * bringing back comparison (but not equality) normalisation * bringing back equality normalisation * Set Version: 1.0.394 * Set Version: 1.0.396 * Set Version: 1.0.398 * removing unsound keccak simplifying assumptions * Set Version: 1.0.399 * Set Version: 1.0.400 * Set Version: 1.0.406 * Set Version: 1.0.407 * adding tests for comparison normalisation, removing keccak * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md Co-authored-by: Everett Hildenbrandt <[email protected]> * ----- alignment * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k --------- Co-authored-by: devops <[email protected]> Co-authored-by: Palina Tolmach <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> Co-authored-by: Tamás Tóth <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
… `#dynBytesArray`
|
Migrated the |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
WIP.
An alternative to the manual approach taken in #2201.
Depends on the runtimeverification/kontrol#303 PR in Kontrol.
In order to generate calldata for functions that contain
bytes,bytes[]parameters, as well as structs with such elements, this PR adds the following toabi.md:#bytesArray(ARRAY_LEN:Int , EACH_ELEMENT_LEN:Int , ELEMENTS:TypedArgs )production, as well as#typeName,#enc,#sizeOfDynamicType,#lenOfHeadrules for itensures lengthBytes(BS) <=Int 1073741824clause to the rule#enc(#bytes(BS)), thereby limiting the possible length of abytesvariable by 1 Gb#encBytes ( Int , TypedArg ),#encodeArgsBytes( TypedArgs, Int ),#encodeArgsAuxBytesRemaining work that has to be done wrt to this PR includes proper struct handling. Previously, our encoding of
#tuple(i.e.,struct) inabi.mdwas based on the assumption that#tupleis a static (not dynamic) elements, and, in this case, the following encoding is correct:However, if a struct contains a dynamically-sized element (e.g.,
bytes data), it gets treated as a dynamic argument: its being stored at an offset, where the elements of a struct are encoded sequentially. For the encoding to work correctly, the encoding and supplementary rules (e.g.,#enc,#sizeOfDynamicType,#lenOfHeads) for tuples should be implemented correctly. To make it easier to define different rules for static and dynamic tuples, this PR added another boolean argument to the#tupleproduction:this value represents whether the struct contains dynamic elements (which is calculated in Kontrol), but there might be a better solution for it.
Finally, this PR also adds
#dynArrayproduction with some dummy rules as a placeholder to avoid failing on (temporarily) unsupported array types, e.g.,tuple[].